\begin{tabbing}
$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $R$:($T$$\rightarrow$$T$$\rightarrow$($T$ List)$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$:$T$. $R$($x$,$x$,[$x$]))
\\[0ex]$\Rightarrow$ \=($\forall$$L$:($T$ List), $x$, $y$, $z$:$T$.\+
\\[0ex]($x$ = $f$($y$)) $\Rightarrow$ ($\neg$($x$ = $y$)) $\Rightarrow$ $R$($y$,$z$,[$y$ / $L$]) $\Rightarrow$ $R$($x$,$z$,[$x$; $y$ / $L$]))
\-\\[0ex]$\Rightarrow$ \{$\forall$$L$:($T$ List), $x$, $y$:$T$. $x$=$f$$\ast$($y$) via $L$ $\Rightarrow$ $R$($x$,$y$,$L$)\}
\end{tabbing}